MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { #equal(@x, @y) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , sortAll(@l) -> sortAll#1(@l) , sortAll#1(::(@x, @xs)) -> sortAll#2(@x, @xs) , sortAll#1(nil()) -> nil() , sortAll#2(tuple#2(@vals, @key), @xs) -> ::(tuple#2(quicksort(@vals), @key), sortAll(@xs)) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitAndSort(@l) -> sortAll(split(@l)) , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Weak Trs: { #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #greater^#(@x, @y) -> c_2(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , append^#(@l, @ys) -> c_3(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_4(append^#(@xs, @ys)) , append#1^#(nil(), @ys) -> c_5() , insert^#(@x, @l) -> c_6(insert#1^#(@x, @l, @x)) , insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_7(insert#2^#(@l, @keyX, @valX, @x)) , insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_8(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , insert#2^#(nil(), @keyX, @valX, @x) -> c_9() , insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_10(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x), #equal^#(@key1, @keyX)) , insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_11(insert^#(@x, @ls)) , insert#4^#(#true(), @key1, @ls, @valX, @vals1, @x) -> c_12() , quicksort^#(@l) -> c_13(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_14(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#1^#(nil()) -> c_15() , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_17(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_16(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_26(splitqs#2^#(splitqs(@pivot, @xs), @pivot, @x), splitqs^#(@pivot, @xs)) , splitqs#1^#(nil(), @pivot) -> c_27() , sortAll^#(@l) -> c_18(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_19(sortAll#2^#(@x, @xs)) , sortAll#1^#(nil()) -> c_20() , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_21(quicksort^#(@vals), sortAll^#(@xs)) , split^#(@l) -> c_22(split#1^#(@l)) , split#1^#(::(@x, @xs)) -> c_23(insert^#(@x, split(@xs)), split^#(@xs)) , split#1^#(nil()) -> c_24() , splitAndSort^#(@l) -> c_25(sortAll^#(split(@l)), split^#(@l)) , splitqs#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_28(splitqs#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , splitqs#3^#(#false(), @ls, @rs, @x) -> c_29() , splitqs#3^#(#true(), @ls, @rs, @x) -> c_30() } Weak DPs: { #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_31(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_32() , #eq^#(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_33() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_34() , #eq^#(nil(), nil()) -> c_35() , #eq^#(nil(), tuple#2(@y_1, @y_2)) -> c_36() , #eq^#(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> c_37() , #eq^#(tuple#2(@x_1, @x_2), nil()) -> c_38() , #eq^#(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_39(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #ckgt^#(#EQ()) -> c_64() , #ckgt^#(#GT()) -> c_65() , #ckgt^#(#LT()) -> c_66() , #compare^#(#0(), #0()) -> c_52() , #compare^#(#0(), #neg(@y)) -> c_53() , #compare^#(#0(), #pos(@y)) -> c_54() , #compare^#(#0(), #s(@y)) -> c_55() , #compare^#(#neg(@x), #0()) -> c_56() , #compare^#(#neg(@x), #neg(@y)) -> c_57(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_58() , #compare^#(#pos(@x), #0()) -> c_59() , #compare^#(#pos(@x), #neg(@y)) -> c_60() , #compare^#(#pos(@x), #pos(@y)) -> c_61(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_62() , #compare^#(#s(@x), #s(@y)) -> c_63(#compare^#(@x, @y)) , #and^#(#false(), #false()) -> c_67() , #and^#(#false(), #true()) -> c_68() , #and^#(#true(), #false()) -> c_69() , #and^#(#true(), #true()) -> c_70() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #greater^#(@x, @y) -> c_2(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , append^#(@l, @ys) -> c_3(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_4(append^#(@xs, @ys)) , append#1^#(nil(), @ys) -> c_5() , insert^#(@x, @l) -> c_6(insert#1^#(@x, @l, @x)) , insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_7(insert#2^#(@l, @keyX, @valX, @x)) , insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_8(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , insert#2^#(nil(), @keyX, @valX, @x) -> c_9() , insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_10(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x), #equal^#(@key1, @keyX)) , insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_11(insert^#(@x, @ls)) , insert#4^#(#true(), @key1, @ls, @valX, @vals1, @x) -> c_12() , quicksort^#(@l) -> c_13(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_14(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#1^#(nil()) -> c_15() , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_17(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_16(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_26(splitqs#2^#(splitqs(@pivot, @xs), @pivot, @x), splitqs^#(@pivot, @xs)) , splitqs#1^#(nil(), @pivot) -> c_27() , sortAll^#(@l) -> c_18(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_19(sortAll#2^#(@x, @xs)) , sortAll#1^#(nil()) -> c_20() , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_21(quicksort^#(@vals), sortAll^#(@xs)) , split^#(@l) -> c_22(split#1^#(@l)) , split#1^#(::(@x, @xs)) -> c_23(insert^#(@x, split(@xs)), split^#(@xs)) , split#1^#(nil()) -> c_24() , splitAndSort^#(@l) -> c_25(sortAll^#(split(@l)), split^#(@l)) , splitqs#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_28(splitqs#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , splitqs#3^#(#false(), @ls, @rs, @x) -> c_29() , splitqs#3^#(#true(), @ls, @rs, @x) -> c_30() } Weak DPs: { #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_31(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_32() , #eq^#(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_33() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_34() , #eq^#(nil(), nil()) -> c_35() , #eq^#(nil(), tuple#2(@y_1, @y_2)) -> c_36() , #eq^#(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> c_37() , #eq^#(tuple#2(@x_1, @x_2), nil()) -> c_38() , #eq^#(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_39(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #ckgt^#(#EQ()) -> c_64() , #ckgt^#(#GT()) -> c_65() , #ckgt^#(#LT()) -> c_66() , #compare^#(#0(), #0()) -> c_52() , #compare^#(#0(), #neg(@y)) -> c_53() , #compare^#(#0(), #pos(@y)) -> c_54() , #compare^#(#0(), #s(@y)) -> c_55() , #compare^#(#neg(@x), #0()) -> c_56() , #compare^#(#neg(@x), #neg(@y)) -> c_57(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_58() , #compare^#(#pos(@x), #0()) -> c_59() , #compare^#(#pos(@x), #neg(@y)) -> c_60() , #compare^#(#pos(@x), #pos(@y)) -> c_61(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_62() , #compare^#(#s(@x), #s(@y)) -> c_63(#compare^#(@x, @y)) , #and^#(#false(), #false()) -> c_67() , #and^#(#false(), #true()) -> c_68() , #and^#(#true(), #false()) -> c_69() , #and^#(#true(), #true()) -> c_70() } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , sortAll(@l) -> sortAll#1(@l) , sortAll#1(::(@x, @xs)) -> sortAll#2(@x, @xs) , sortAll#1(nil()) -> nil() , sortAll#2(tuple#2(@vals, @key), @xs) -> ::(tuple#2(quicksort(@vals), @key), sortAll(@xs)) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitAndSort(@l) -> sortAll(split(@l)) , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,5,9,12,15,19,22,26,29,30} by applications of Pre({1,2,5,9,12,15,19,22,26,29,30}) = {3,7,10,13,17,20,24,28}. Here rules are labeled as follows: DPs: { 1: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , 2: #greater^#(@x, @y) -> c_2(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 3: append^#(@l, @ys) -> c_3(append#1^#(@l, @ys)) , 4: append#1^#(::(@x, @xs), @ys) -> c_4(append^#(@xs, @ys)) , 5: append#1^#(nil(), @ys) -> c_5() , 6: insert^#(@x, @l) -> c_6(insert#1^#(@x, @l, @x)) , 7: insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_7(insert#2^#(@l, @keyX, @valX, @x)) , 8: insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_8(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , 9: insert#2^#(nil(), @keyX, @valX, @x) -> c_9() , 10: insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_10(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x), #equal^#(@key1, @keyX)) , 11: insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_11(insert^#(@x, @ls)) , 12: insert#4^#(#true(), @key1, @ls, @valX, @vals1, @x) -> c_12() , 13: quicksort^#(@l) -> c_13(quicksort#1^#(@l)) , 14: quicksort#1^#(::(@z, @zs)) -> c_14(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , 15: quicksort#1^#(nil()) -> c_15() , 16: quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_17(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , 17: splitqs^#(@pivot, @l) -> c_16(splitqs#1^#(@l, @pivot)) , 18: splitqs#1^#(::(@x, @xs), @pivot) -> c_26(splitqs#2^#(splitqs(@pivot, @xs), @pivot, @x), splitqs^#(@pivot, @xs)) , 19: splitqs#1^#(nil(), @pivot) -> c_27() , 20: sortAll^#(@l) -> c_18(sortAll#1^#(@l)) , 21: sortAll#1^#(::(@x, @xs)) -> c_19(sortAll#2^#(@x, @xs)) , 22: sortAll#1^#(nil()) -> c_20() , 23: sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_21(quicksort^#(@vals), sortAll^#(@xs)) , 24: split^#(@l) -> c_22(split#1^#(@l)) , 25: split#1^#(::(@x, @xs)) -> c_23(insert^#(@x, split(@xs)), split^#(@xs)) , 26: split#1^#(nil()) -> c_24() , 27: splitAndSort^#(@l) -> c_25(sortAll^#(split(@l)), split^#(@l)) , 28: splitqs#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_28(splitqs#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , 29: splitqs#3^#(#false(), @ls, @rs, @x) -> c_29() , 30: splitqs#3^#(#true(), @ls, @rs, @x) -> c_30() , 31: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_31(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 32: #eq^#(::(@x_1, @x_2), nil()) -> c_32() , 33: #eq^#(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_33() , 34: #eq^#(nil(), ::(@y_1, @y_2)) -> c_34() , 35: #eq^#(nil(), nil()) -> c_35() , 36: #eq^#(nil(), tuple#2(@y_1, @y_2)) -> c_36() , 37: #eq^#(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> c_37() , 38: #eq^#(tuple#2(@x_1, @x_2), nil()) -> c_38() , 39: #eq^#(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_39(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 40: #eq^#(#0(), #0()) -> c_40() , 41: #eq^#(#0(), #neg(@y)) -> c_41() , 42: #eq^#(#0(), #pos(@y)) -> c_42() , 43: #eq^#(#0(), #s(@y)) -> c_43() , 44: #eq^#(#neg(@x), #0()) -> c_44() , 45: #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , 46: #eq^#(#neg(@x), #pos(@y)) -> c_46() , 47: #eq^#(#pos(@x), #0()) -> c_47() , 48: #eq^#(#pos(@x), #neg(@y)) -> c_48() , 49: #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , 50: #eq^#(#s(@x), #0()) -> c_50() , 51: #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , 52: #ckgt^#(#EQ()) -> c_64() , 53: #ckgt^#(#GT()) -> c_65() , 54: #ckgt^#(#LT()) -> c_66() , 55: #compare^#(#0(), #0()) -> c_52() , 56: #compare^#(#0(), #neg(@y)) -> c_53() , 57: #compare^#(#0(), #pos(@y)) -> c_54() , 58: #compare^#(#0(), #s(@y)) -> c_55() , 59: #compare^#(#neg(@x), #0()) -> c_56() , 60: #compare^#(#neg(@x), #neg(@y)) -> c_57(#compare^#(@y, @x)) , 61: #compare^#(#neg(@x), #pos(@y)) -> c_58() , 62: #compare^#(#pos(@x), #0()) -> c_59() , 63: #compare^#(#pos(@x), #neg(@y)) -> c_60() , 64: #compare^#(#pos(@x), #pos(@y)) -> c_61(#compare^#(@x, @y)) , 65: #compare^#(#s(@x), #0()) -> c_62() , 66: #compare^#(#s(@x), #s(@y)) -> c_63(#compare^#(@x, @y)) , 67: #and^#(#false(), #false()) -> c_67() , 68: #and^#(#false(), #true()) -> c_68() , 69: #and^#(#true(), #false()) -> c_69() , 70: #and^#(#true(), #true()) -> c_70() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(@l, @ys) -> c_3(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_4(append^#(@xs, @ys)) , insert^#(@x, @l) -> c_6(insert#1^#(@x, @l, @x)) , insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_7(insert#2^#(@l, @keyX, @valX, @x)) , insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_8(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_10(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x), #equal^#(@key1, @keyX)) , insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_11(insert^#(@x, @ls)) , quicksort^#(@l) -> c_13(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_14(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_17(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_16(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_26(splitqs#2^#(splitqs(@pivot, @xs), @pivot, @x), splitqs^#(@pivot, @xs)) , sortAll^#(@l) -> c_18(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_19(sortAll#2^#(@x, @xs)) , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_21(quicksort^#(@vals), sortAll^#(@xs)) , split^#(@l) -> c_22(split#1^#(@l)) , split#1^#(::(@x, @xs)) -> c_23(insert^#(@x, split(@xs)), split^#(@xs)) , splitAndSort^#(@l) -> c_25(sortAll^#(split(@l)), split^#(@l)) , splitqs#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_28(splitqs#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) } Weak DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_31(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_32() , #eq^#(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_33() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_34() , #eq^#(nil(), nil()) -> c_35() , #eq^#(nil(), tuple#2(@y_1, @y_2)) -> c_36() , #eq^#(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> c_37() , #eq^#(tuple#2(@x_1, @x_2), nil()) -> c_38() , #eq^#(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_39(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #greater^#(@x, @y) -> c_2(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_64() , #ckgt^#(#GT()) -> c_65() , #ckgt^#(#LT()) -> c_66() , #compare^#(#0(), #0()) -> c_52() , #compare^#(#0(), #neg(@y)) -> c_53() , #compare^#(#0(), #pos(@y)) -> c_54() , #compare^#(#0(), #s(@y)) -> c_55() , #compare^#(#neg(@x), #0()) -> c_56() , #compare^#(#neg(@x), #neg(@y)) -> c_57(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_58() , #compare^#(#pos(@x), #0()) -> c_59() , #compare^#(#pos(@x), #neg(@y)) -> c_60() , #compare^#(#pos(@x), #pos(@y)) -> c_61(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_62() , #compare^#(#s(@x), #s(@y)) -> c_63(#compare^#(@x, @y)) , append#1^#(nil(), @ys) -> c_5() , insert#2^#(nil(), @keyX, @valX, @x) -> c_9() , insert#4^#(#true(), @key1, @ls, @valX, @vals1, @x) -> c_12() , quicksort#1^#(nil()) -> c_15() , splitqs#1^#(nil(), @pivot) -> c_27() , sortAll#1^#(nil()) -> c_20() , split#1^#(nil()) -> c_24() , splitqs#3^#(#false(), @ls, @rs, @x) -> c_29() , splitqs#3^#(#true(), @ls, @rs, @x) -> c_30() , #and^#(#false(), #false()) -> c_67() , #and^#(#false(), #true()) -> c_68() , #and^#(#true(), #false()) -> c_69() , #and^#(#true(), #true()) -> c_70() } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , sortAll(@l) -> sortAll#1(@l) , sortAll#1(::(@x, @xs)) -> sortAll#2(@x, @xs) , sortAll#1(nil()) -> nil() , sortAll#2(tuple#2(@vals, @key), @xs) -> ::(tuple#2(quicksort(@vals), @key), sortAll(@xs)) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitAndSort(@l) -> sortAll(split(@l)) , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {19} by applications of Pre({19}) = {12}. Here rules are labeled as follows: DPs: { 1: append^#(@l, @ys) -> c_3(append#1^#(@l, @ys)) , 2: append#1^#(::(@x, @xs), @ys) -> c_4(append^#(@xs, @ys)) , 3: insert^#(@x, @l) -> c_6(insert#1^#(@x, @l, @x)) , 4: insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_7(insert#2^#(@l, @keyX, @valX, @x)) , 5: insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_8(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , 6: insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_10(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x), #equal^#(@key1, @keyX)) , 7: insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_11(insert^#(@x, @ls)) , 8: quicksort^#(@l) -> c_13(quicksort#1^#(@l)) , 9: quicksort#1^#(::(@z, @zs)) -> c_14(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , 10: quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_17(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , 11: splitqs^#(@pivot, @l) -> c_16(splitqs#1^#(@l, @pivot)) , 12: splitqs#1^#(::(@x, @xs), @pivot) -> c_26(splitqs#2^#(splitqs(@pivot, @xs), @pivot, @x), splitqs^#(@pivot, @xs)) , 13: sortAll^#(@l) -> c_18(sortAll#1^#(@l)) , 14: sortAll#1^#(::(@x, @xs)) -> c_19(sortAll#2^#(@x, @xs)) , 15: sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_21(quicksort^#(@vals), sortAll^#(@xs)) , 16: split^#(@l) -> c_22(split#1^#(@l)) , 17: split#1^#(::(@x, @xs)) -> c_23(insert^#(@x, split(@xs)), split^#(@xs)) , 18: splitAndSort^#(@l) -> c_25(sortAll^#(split(@l)), split^#(@l)) , 19: splitqs#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_28(splitqs#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , 20: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , 21: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_31(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 22: #eq^#(::(@x_1, @x_2), nil()) -> c_32() , 23: #eq^#(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_33() , 24: #eq^#(nil(), ::(@y_1, @y_2)) -> c_34() , 25: #eq^#(nil(), nil()) -> c_35() , 26: #eq^#(nil(), tuple#2(@y_1, @y_2)) -> c_36() , 27: #eq^#(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> c_37() , 28: #eq^#(tuple#2(@x_1, @x_2), nil()) -> c_38() , 29: #eq^#(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_39(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 30: #eq^#(#0(), #0()) -> c_40() , 31: #eq^#(#0(), #neg(@y)) -> c_41() , 32: #eq^#(#0(), #pos(@y)) -> c_42() , 33: #eq^#(#0(), #s(@y)) -> c_43() , 34: #eq^#(#neg(@x), #0()) -> c_44() , 35: #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , 36: #eq^#(#neg(@x), #pos(@y)) -> c_46() , 37: #eq^#(#pos(@x), #0()) -> c_47() , 38: #eq^#(#pos(@x), #neg(@y)) -> c_48() , 39: #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , 40: #eq^#(#s(@x), #0()) -> c_50() , 41: #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , 42: #greater^#(@x, @y) -> c_2(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 43: #ckgt^#(#EQ()) -> c_64() , 44: #ckgt^#(#GT()) -> c_65() , 45: #ckgt^#(#LT()) -> c_66() , 46: #compare^#(#0(), #0()) -> c_52() , 47: #compare^#(#0(), #neg(@y)) -> c_53() , 48: #compare^#(#0(), #pos(@y)) -> c_54() , 49: #compare^#(#0(), #s(@y)) -> c_55() , 50: #compare^#(#neg(@x), #0()) -> c_56() , 51: #compare^#(#neg(@x), #neg(@y)) -> c_57(#compare^#(@y, @x)) , 52: #compare^#(#neg(@x), #pos(@y)) -> c_58() , 53: #compare^#(#pos(@x), #0()) -> c_59() , 54: #compare^#(#pos(@x), #neg(@y)) -> c_60() , 55: #compare^#(#pos(@x), #pos(@y)) -> c_61(#compare^#(@x, @y)) , 56: #compare^#(#s(@x), #0()) -> c_62() , 57: #compare^#(#s(@x), #s(@y)) -> c_63(#compare^#(@x, @y)) , 58: append#1^#(nil(), @ys) -> c_5() , 59: insert#2^#(nil(), @keyX, @valX, @x) -> c_9() , 60: insert#4^#(#true(), @key1, @ls, @valX, @vals1, @x) -> c_12() , 61: quicksort#1^#(nil()) -> c_15() , 62: splitqs#1^#(nil(), @pivot) -> c_27() , 63: sortAll#1^#(nil()) -> c_20() , 64: split#1^#(nil()) -> c_24() , 65: splitqs#3^#(#false(), @ls, @rs, @x) -> c_29() , 66: splitqs#3^#(#true(), @ls, @rs, @x) -> c_30() , 67: #and^#(#false(), #false()) -> c_67() , 68: #and^#(#false(), #true()) -> c_68() , 69: #and^#(#true(), #false()) -> c_69() , 70: #and^#(#true(), #true()) -> c_70() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(@l, @ys) -> c_3(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_4(append^#(@xs, @ys)) , insert^#(@x, @l) -> c_6(insert#1^#(@x, @l, @x)) , insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_7(insert#2^#(@l, @keyX, @valX, @x)) , insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_8(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_10(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x), #equal^#(@key1, @keyX)) , insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_11(insert^#(@x, @ls)) , quicksort^#(@l) -> c_13(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_14(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_17(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_16(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_26(splitqs#2^#(splitqs(@pivot, @xs), @pivot, @x), splitqs^#(@pivot, @xs)) , sortAll^#(@l) -> c_18(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_19(sortAll#2^#(@x, @xs)) , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_21(quicksort^#(@vals), sortAll^#(@xs)) , split^#(@l) -> c_22(split#1^#(@l)) , split#1^#(::(@x, @xs)) -> c_23(insert^#(@x, split(@xs)), split^#(@xs)) , splitAndSort^#(@l) -> c_25(sortAll^#(split(@l)), split^#(@l)) } Weak DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_31(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_32() , #eq^#(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_33() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_34() , #eq^#(nil(), nil()) -> c_35() , #eq^#(nil(), tuple#2(@y_1, @y_2)) -> c_36() , #eq^#(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> c_37() , #eq^#(tuple#2(@x_1, @x_2), nil()) -> c_38() , #eq^#(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_39(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #greater^#(@x, @y) -> c_2(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_64() , #ckgt^#(#GT()) -> c_65() , #ckgt^#(#LT()) -> c_66() , #compare^#(#0(), #0()) -> c_52() , #compare^#(#0(), #neg(@y)) -> c_53() , #compare^#(#0(), #pos(@y)) -> c_54() , #compare^#(#0(), #s(@y)) -> c_55() , #compare^#(#neg(@x), #0()) -> c_56() , #compare^#(#neg(@x), #neg(@y)) -> c_57(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_58() , #compare^#(#pos(@x), #0()) -> c_59() , #compare^#(#pos(@x), #neg(@y)) -> c_60() , #compare^#(#pos(@x), #pos(@y)) -> c_61(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_62() , #compare^#(#s(@x), #s(@y)) -> c_63(#compare^#(@x, @y)) , append#1^#(nil(), @ys) -> c_5() , insert#2^#(nil(), @keyX, @valX, @x) -> c_9() , insert#4^#(#true(), @key1, @ls, @valX, @vals1, @x) -> c_12() , quicksort#1^#(nil()) -> c_15() , splitqs#1^#(nil(), @pivot) -> c_27() , sortAll#1^#(nil()) -> c_20() , split#1^#(nil()) -> c_24() , splitqs#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_28(splitqs#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , splitqs#3^#(#false(), @ls, @rs, @x) -> c_29() , splitqs#3^#(#true(), @ls, @rs, @x) -> c_30() , #and^#(#false(), #false()) -> c_67() , #and^#(#false(), #true()) -> c_68() , #and^#(#true(), #false()) -> c_69() , #and^#(#true(), #true()) -> c_70() } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , sortAll(@l) -> sortAll#1(@l) , sortAll#1(::(@x, @xs)) -> sortAll#2(@x, @xs) , sortAll#1(nil()) -> nil() , sortAll#2(tuple#2(@vals, @key), @xs) -> ::(tuple#2(quicksort(@vals), @key), sortAll(@xs)) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitAndSort(@l) -> sortAll(split(@l)) , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_31(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_32() , #eq^#(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_33() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_34() , #eq^#(nil(), nil()) -> c_35() , #eq^#(nil(), tuple#2(@y_1, @y_2)) -> c_36() , #eq^#(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> c_37() , #eq^#(tuple#2(@x_1, @x_2), nil()) -> c_38() , #eq^#(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> c_39(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #greater^#(@x, @y) -> c_2(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_64() , #ckgt^#(#GT()) -> c_65() , #ckgt^#(#LT()) -> c_66() , #compare^#(#0(), #0()) -> c_52() , #compare^#(#0(), #neg(@y)) -> c_53() , #compare^#(#0(), #pos(@y)) -> c_54() , #compare^#(#0(), #s(@y)) -> c_55() , #compare^#(#neg(@x), #0()) -> c_56() , #compare^#(#neg(@x), #neg(@y)) -> c_57(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_58() , #compare^#(#pos(@x), #0()) -> c_59() , #compare^#(#pos(@x), #neg(@y)) -> c_60() , #compare^#(#pos(@x), #pos(@y)) -> c_61(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_62() , #compare^#(#s(@x), #s(@y)) -> c_63(#compare^#(@x, @y)) , append#1^#(nil(), @ys) -> c_5() , insert#2^#(nil(), @keyX, @valX, @x) -> c_9() , insert#4^#(#true(), @key1, @ls, @valX, @vals1, @x) -> c_12() , quicksort#1^#(nil()) -> c_15() , splitqs#1^#(nil(), @pivot) -> c_27() , sortAll#1^#(nil()) -> c_20() , split#1^#(nil()) -> c_24() , splitqs#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_28(splitqs#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , splitqs#3^#(#false(), @ls, @rs, @x) -> c_29() , splitqs#3^#(#true(), @ls, @rs, @x) -> c_30() , #and^#(#false(), #false()) -> c_67() , #and^#(#false(), #true()) -> c_68() , #and^#(#true(), #false()) -> c_69() , #and^#(#true(), #true()) -> c_70() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(@l, @ys) -> c_3(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_4(append^#(@xs, @ys)) , insert^#(@x, @l) -> c_6(insert#1^#(@x, @l, @x)) , insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_7(insert#2^#(@l, @keyX, @valX, @x)) , insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_8(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_10(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x), #equal^#(@key1, @keyX)) , insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_11(insert^#(@x, @ls)) , quicksort^#(@l) -> c_13(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_14(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_17(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_16(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_26(splitqs#2^#(splitqs(@pivot, @xs), @pivot, @x), splitqs^#(@pivot, @xs)) , sortAll^#(@l) -> c_18(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_19(sortAll#2^#(@x, @xs)) , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_21(quicksort^#(@vals), sortAll^#(@xs)) , split^#(@l) -> c_22(split#1^#(@l)) , split#1^#(::(@x, @xs)) -> c_23(insert^#(@x, split(@xs)), split^#(@xs)) , splitAndSort^#(@l) -> c_25(sortAll^#(split(@l)), split^#(@l)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , sortAll(@l) -> sortAll#1(@l) , sortAll#1(::(@x, @xs)) -> sortAll#2(@x, @xs) , sortAll#1(nil()) -> nil() , sortAll#2(tuple#2(@vals, @key), @xs) -> ::(tuple#2(quicksort(@vals), @key), sortAll(@xs)) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitAndSort(@l) -> sortAll(split(@l)) , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_10(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x), #equal^#(@key1, @keyX)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_26(splitqs#2^#(splitqs(@pivot, @xs), @pivot, @x), splitqs^#(@pivot, @xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , insert^#(@x, @l) -> c_3(insert#1^#(@x, @l, @x)) , insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_4(insert#2^#(@l, @keyX, @valX, @x)) , insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_5(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_6(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)) , insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_7(insert^#(@x, @ls)) , quicksort^#(@l) -> c_8(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_9(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_10(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_11(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_12(splitqs^#(@pivot, @xs)) , sortAll^#(@l) -> c_13(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_14(sortAll#2^#(@x, @xs)) , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_15(quicksort^#(@vals), sortAll^#(@xs)) , split^#(@l) -> c_16(split#1^#(@l)) , split#1^#(::(@x, @xs)) -> c_17(insert^#(@x, split(@xs)), split^#(@xs)) , splitAndSort^#(@l) -> c_18(sortAll^#(split(@l)), split^#(@l)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , sortAll(@l) -> sortAll#1(@l) , sortAll#1(::(@x, @xs)) -> sortAll#2(@x, @xs) , sortAll#1(nil()) -> nil() , sortAll#2(tuple#2(@vals, @key), @xs) -> ::(tuple#2(quicksort(@vals), @key), sortAll(@xs)) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitAndSort(@l) -> sortAll(split(@l)) , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , insert^#(@x, @l) -> c_3(insert#1^#(@x, @l, @x)) , insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_4(insert#2^#(@l, @keyX, @valX, @x)) , insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_5(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_6(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)) , insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_7(insert^#(@x, @ls)) , quicksort^#(@l) -> c_8(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_9(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_10(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_11(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_12(splitqs^#(@pivot, @xs)) , sortAll^#(@l) -> c_13(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_14(sortAll#2^#(@x, @xs)) , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_15(quicksort^#(@vals), sortAll^#(@xs)) , split^#(@l) -> c_16(split#1^#(@l)) , split#1^#(::(@x, @xs)) -> c_17(insert^#(@x, split(@xs)), split^#(@xs)) , splitAndSort^#(@l) -> c_18(sortAll^#(split(@l)), split^#(@l)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. DPs: { 6: insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_6(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)) } Trs: { #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#LT()) -> #false() , append#1(nil(), @ys) -> @ys , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort#1(nil()) -> nil() , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#true(), #true()) -> #true() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1, 2}, Uargs(c_10) = {1, 2, 3}, Uargs(c_11) = {1}, Uargs(c_12) = {1}, Uargs(c_13) = {1}, Uargs(c_14) = {1}, Uargs(c_15) = {1, 2}, Uargs(c_16) = {1}, Uargs(c_17) = {1, 2}, Uargs(c_18) = {1, 2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#equal](x1, x2) = [2] [0] [#eq](x1, x2) = [0 0] x1 + [1] [1 0] [2] [#greater](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [1 0] [1 0] [2] [#compare](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] [#ckgt](x1) = [1 0] x1 + [0] [1 1] [0] [append](x1, x2) = [0 0] x1 + [0 1] x2 + [0] [0 1] [1 1] [1] [append#1](x1, x2) = [1 1] x1 + [1 0] x2 + [2] [0 1] [0 1] [2] [::](x1, x2) = [1 0] x1 + [1 1] x2 + [0] [0 0] [0 1] [1] [nil] = [2] [0] [insert](x1, x2) = [1 1] x2 + [1] [0 1] [1] [insert#1](x1, x2, x3) = [1 1] x2 + [1] [0 1] [1] [tuple#2](x1, x2) = [0 1] x1 + [0] [0 1] [0] [insert#2](x1, x2, x3, x4) = [1 1] x1 + [1] [0 1] [1] [insert#3](x1, x2, x3, x4, x5) = [1 0] x1 + [1 2] x3 + [2] [0 0] [0 1] [2] [insert#4](x1, x2, x3, x4, x5, x6) = [1 2] x3 + [0 1] x5 + [2] [0 1] [0 0] [2] [#false] = [1] [1] [#true] = [0] [1] [quicksort](x1) = [2] [0] [quicksort#1](x1) = [1 0] x1 + [2] [0 0] [0] [splitqs](x1, x2) = [0 0] x1 + [1 2] x2 + [1] [2 0] [2 2] [1] [quicksort#2](x1, x2) = [1 0] x2 + [2] [0 0] [0] [sortAll](x1) = [0] [0] [sortAll#1](x1) = [0] [0] [sortAll#2](x1, x2) = [0] [0] [split](x1) = [1 2] x1 + [2] [0 1] [0] [split#1](x1) = [1 2] x1 + [2] [0 1] [0] [splitAndSort](x1) = [0] [0] [splitqs#1](x1, x2) = [1 2] x1 + [0 0] x2 + [1] [2 2] [2 0] [0] [splitqs#2](x1, x2, x3) = [1 0] x1 + [0 0] x2 + [1 0] x3 + [2] [2 0] [2 0] [2 0] [0] [splitqs#3](x1, x2, x3, x4) = [0 0] x1 + [0 1] x2 + [2] [2 0] [0 1] [0] [#and](x1, x2) = [1] [2] [#EQ] = [1] [1] [#GT] = [0] [1] [#LT] = [2] [0] [#0] = [1] [2] [#neg](x1) = [1 0] x1 + [1] [0 0] [2] [#pos](x1) = [1 0] x1 + [1] [0 1] [2] [#s](x1) = [1 0] x1 + [2] [0 1] [2] [#equal^#](x1, x2) = [0] [0] [c_1](x1) = [0] [0] [#eq^#](x1, x2) = [0] [0] [#greater^#](x1, x2) = [0] [0] [c_2](x1, x2) = [0] [0] [#ckgt^#](x1) = [0] [0] [#compare^#](x1, x2) = [0] [0] [append^#](x1, x2) = [0] [0] [c_3](x1) = [0] [0] [append#1^#](x1, x2) = [0] [0] [c_4](x1) = [0] [0] [c_5] = [0] [0] [insert^#](x1, x2) = [0 1] x2 + [0] [0 0] [1] [c_6](x1) = [0] [0] [insert#1^#](x1, x2, x3) = [0 1] x2 + [0] [0 0] [0] [c_7](x1) = [0] [0] [insert#2^#](x1, x2, x3, x4) = [0 1] x1 + [0 0] x2 + [0] [0 0] [1 1] [0] [c_8](x1) = [0] [0] [insert#3^#](x1, x2, x3, x4, x5) = [0 1] x3 + [1] [0 0] [1] [c_9] = [0] [0] [c_10](x1, x2) = [0] [0] [insert#4^#](x1, x2, x3, x4, x5, x6) = [0 1] x3 + [0] [0 0] [0] [c_11](x1) = [0] [0] [c_12] = [0] [0] [quicksort^#](x1) = [0] [0] [c_13](x1) = [0] [0] [quicksort#1^#](x1) = [0] [0] [c_14](x1, x2) = [0] [0] [quicksort#2^#](x1, x2) = [0] [0] [splitqs^#](x1, x2) = [0] [0] [c_15] = [0] [0] [c_16](x1) = [0] [0] [splitqs#1^#](x1, x2) = [0] [0] [c_17](x1, x2, x3) = [0] [0] [sortAll^#](x1) = [2] [0] [c_18](x1) = [0] [0] [sortAll#1^#](x1) = [2] [0] [c_19](x1) = [0] [0] [sortAll#2^#](x1, x2) = [0 0] x1 + [0 0] x2 + [2] [0 1] [1 1] [0] [c_20] = [0] [0] [c_21](x1, x2) = [0] [0] [split^#](x1) = [1 1] x1 + [0] [0 1] [0] [c_22](x1) = [0] [0] [split#1^#](x1) = [1 1] x1 + [0] [0 0] [0] [c_23](x1, x2) = [0] [0] [c_24] = [0] [0] [splitAndSort^#](x1) = [2 2] x1 + [2] [1 2] [1] [c_25](x1, x2) = [0] [0] [c_26](x1, x2) = [0] [0] [splitqs#2^#](x1, x2, x3) = [0] [0] [c_27] = [0] [0] [c_28](x1, x2) = [0] [0] [splitqs#3^#](x1, x2, x3, x4) = [0] [0] [c_29] = [0] [0] [c_30] = [0] [0] [c_31](x1, x2, x3) = [0] [0] [#and^#](x1, x2) = [0] [0] [c_32] = [0] [0] [c_33] = [0] [0] [c_34] = [0] [0] [c_35] = [0] [0] [c_36] = [0] [0] [c_37] = [0] [0] [c_38] = [0] [0] [c_39](x1, x2, x3) = [0] [0] [c_40] = [0] [0] [c_41] = [0] [0] [c_42] = [0] [0] [c_43] = [0] [0] [c_44] = [0] [0] [c_45](x1) = [0] [0] [c_46] = [0] [0] [c_47] = [0] [0] [c_48] = [0] [0] [c_49](x1) = [0] [0] [c_50] = [0] [0] [c_51](x1) = [0] [0] [c_52] = [0] [0] [c_53] = [0] [0] [c_54] = [0] [0] [c_55] = [0] [0] [c_56] = [0] [0] [c_57](x1) = [0] [0] [c_58] = [0] [0] [c_59] = [0] [0] [c_60] = [0] [0] [c_61](x1) = [0] [0] [c_62] = [0] [0] [c_63](x1) = [0] [0] [c_64] = [0] [0] [c_65] = [0] [0] [c_66] = [0] [0] [c_67] = [0] [0] [c_68] = [0] [0] [c_69] = [0] [0] [c_70] = [0] [0] [c] = [0] [0] [c_1](x1) = [1 0] x1 + [0] [0 0] [0] [c_2](x1) = [1 0] x1 + [0] [0 0] [0] [c_3](x1) = [1 0] x1 + [0] [0 0] [0] [c_4](x1) = [1 0] x1 + [0] [0 0] [0] [c_5](x1) = [1 0] x1 + [0] [0 0] [0] [c_6](x1) = [1 1] x1 + [0] [0 0] [0] [c_7](x1) = [1 0] x1 + [0] [0 0] [0] [c_8](x1) = [1 0] x1 + [0] [0 0] [0] [c_9](x1, x2) = [1 0] x1 + [1 1] x2 + [0] [0 0] [0 0] [0] [c_10](x1, x2, x3) = [1 0] x1 + [1 1] x2 + [1 0] x3 + [0] [0 0] [0 0] [0 0] [0] [c_11](x1) = [1 1] x1 + [0] [0 0] [0] [c_12](x1) = [1 1] x1 + [0] [0 0] [0] [c_13](x1) = [1 0] x1 + [0] [0 0] [0] [c_14](x1) = [1 0] x1 + [0] [0 0] [0] [c_15](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [c_16](x1) = [1 0] x1 + [0] [0 0] [0] [c_17](x1, x2) = [1 1] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [c_18](x1, x2) = [1 1] x1 + [2 0] x2 + [0] [0 0] [0 0] [1] This order satisfies following ordering constraints [#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [0 0] @x_1 + [0 0] @x_2 + [1] [1 0] [1 1] [2] >= [1] [2] = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] [#eq(::(@x_1, @x_2), nil())] = [0 0] @x_1 + [0 0] @x_2 + [1] [1 0] [1 1] [2] >= [1] [1] = [#false()] [#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2))] = [0 0] @x_1 + [0 0] @x_2 + [1] [1 0] [1 1] [2] >= [1] [1] = [#false()] [#eq(nil(), ::(@y_1, @y_2))] = [1] [4] >= [1] [1] = [#false()] [#eq(nil(), nil())] = [1] [4] > [0] [1] = [#true()] [#eq(nil(), tuple#2(@y_1, @y_2))] = [1] [4] >= [1] [1] = [#false()] [#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2))] = [0 0] @x_1 + [1] [0 1] [2] >= [1] [1] = [#false()] [#eq(tuple#2(@x_1, @x_2), nil())] = [0 0] @x_1 + [1] [0 1] [2] >= [1] [1] = [#false()] [#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2))] = [0 0] @x_1 + [1] [0 1] [2] >= [1] [2] = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] [#eq(#0(), #0())] = [1] [3] > [0] [1] = [#true()] [#eq(#0(), #neg(@y))] = [1] [3] >= [1] [1] = [#false()] [#eq(#0(), #pos(@y))] = [1] [3] >= [1] [1] = [#false()] [#eq(#0(), #s(@y))] = [1] [3] >= [1] [1] = [#false()] [#eq(#neg(@x), #0())] = [0 0] @x + [1] [1 0] [3] >= [1] [1] = [#false()] [#eq(#neg(@x), #neg(@y))] = [0 0] @x + [1] [1 0] [3] >= [0 0] @x + [1] [1 0] [2] = [#eq(@x, @y)] [#eq(#neg(@x), #pos(@y))] = [0 0] @x + [1] [1 0] [3] >= [1] [1] = [#false()] [#eq(#pos(@x), #0())] = [0 0] @x + [1] [1 0] [3] >= [1] [1] = [#false()] [#eq(#pos(@x), #neg(@y))] = [0 0] @x + [1] [1 0] [3] >= [1] [1] = [#false()] [#eq(#pos(@x), #pos(@y))] = [0 0] @x + [1] [1 0] [3] >= [0 0] @x + [1] [1 0] [2] = [#eq(@x, @y)] [#eq(#s(@x), #0())] = [0 0] @x + [1] [1 0] [4] >= [1] [1] = [#false()] [#eq(#s(@x), #s(@y))] = [0 0] @x + [1] [1 0] [4] >= [0 0] @x + [1] [1 0] [2] = [#eq(@x, @y)] [#greater(@x, @y)] = [1 0] @x + [1 0] @y + [0] [1 0] [1 0] [2] >= [1 0] @x + [1 0] @y + [0] [1 0] [1 0] [1] = [#ckgt(#compare(@x, @y))] [#compare(#0(), #0())] = [2] [1] > [1] [1] = [#EQ()] [#compare(#0(), #neg(@y))] = [1 0] @y + [2] [0 0] [1] > [0] [1] = [#GT()] [#compare(#0(), #pos(@y))] = [1 0] @y + [2] [0 0] [1] >= [2] [0] = [#LT()] [#compare(#0(), #s(@y))] = [1 0] @y + [3] [0 0] [1] > [2] [0] = [#LT()] [#compare(#neg(@x), #0())] = [1 0] @x + [2] [0 0] [1] >= [2] [0] = [#LT()] [#compare(#neg(@x), #neg(@y))] = [1 0] @x + [1 0] @y + [2] [0 0] [0 0] [1] > [1 0] @x + [1 0] @y + [0] [0 0] [0 0] [1] = [#compare(@y, @x)] [#compare(#neg(@x), #pos(@y))] = [1 0] @x + [1 0] @y + [2] [0 0] [0 0] [1] >= [2] [0] = [#LT()] [#compare(#pos(@x), #0())] = [1 0] @x + [2] [0 0] [1] > [0] [1] = [#GT()] [#compare(#pos(@x), #neg(@y))] = [1 0] @x + [1 0] @y + [2] [0 0] [0 0] [1] > [0] [1] = [#GT()] [#compare(#pos(@x), #pos(@y))] = [1 0] @x + [1 0] @y + [2] [0 0] [0 0] [1] > [1 0] @x + [1 0] @y + [0] [0 0] [0 0] [1] = [#compare(@x, @y)] [#compare(#s(@x), #0())] = [1 0] @x + [3] [0 0] [1] > [0] [1] = [#GT()] [#compare(#s(@x), #s(@y))] = [1 0] @x + [1 0] @y + [4] [0 0] [0 0] [1] > [1 0] @x + [1 0] @y + [0] [0 0] [0 0] [1] = [#compare(@x, @y)] [#ckgt(#EQ())] = [1] [2] >= [1] [1] = [#false()] [#ckgt(#GT())] = [0] [1] >= [0] [1] = [#true()] [#ckgt(#LT())] = [2] [2] > [1] [1] = [#false()] [insert(@x, @l)] = [1 1] @l + [1] [0 1] [1] >= [1 1] @l + [1] [0 1] [1] = [insert#1(@x, @l, @x)] [insert#1(tuple#2(@valX, @keyX), @l, @x)] = [1 1] @l + [1] [0 1] [1] >= [1 1] @l + [1] [0 1] [1] = [insert#2(@l, @keyX, @valX, @x)] [insert#2(::(@l1, @ls), @keyX, @valX, @x)] = [1 0] @l1 + [1 2] @ls + [2] [0 0] [0 1] [2] >= [1 0] @l1 + [1 2] @ls + [2] [0 0] [0 1] [2] = [insert#3(@l1, @keyX, @ls, @valX, @x)] [insert#2(nil(), @keyX, @valX, @x)] = [3] [1] >= [3] [1] = [::(tuple#2(::(@valX, nil()), @keyX), nil())] [insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x)] = [1 2] @ls + [0 1] @vals1 + [2] [0 1] [0 0] [2] >= [1 2] @ls + [0 1] @vals1 + [2] [0 1] [0 0] [2] = [insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)] [insert#4(#false(), @key1, @ls, @valX, @vals1, @x)] = [1 2] @ls + [0 1] @vals1 + [2] [0 1] [0 0] [2] >= [1 2] @ls + [0 1] @vals1 + [2] [0 1] [0 0] [2] = [::(tuple#2(@vals1, @key1), insert(@x, @ls))] [insert#4(#true(), @key1, @ls, @valX, @vals1, @x)] = [1 2] @ls + [0 1] @vals1 + [2] [0 1] [0 0] [2] > [1 1] @ls + [0 1] @vals1 + [1] [0 1] [0 0] [1] = [::(tuple#2(::(@valX, @vals1), @key1), @ls)] [splitqs(@pivot, @l)] = [1 2] @l + [0 0] @pivot + [1] [2 2] [2 0] [1] >= [1 2] @l + [0 0] @pivot + [1] [2 2] [2 0] [0] = [splitqs#1(@l, @pivot)] [split(@l)] = [1 2] @l + [2] [0 1] [0] >= [1 2] @l + [2] [0 1] [0] = [split#1(@l)] [split#1(::(@x, @xs))] = [1 0] @x + [1 3] @xs + [4] [0 0] [0 1] [1] > [1 3] @xs + [3] [0 1] [1] = [insert(@x, split(@xs))] [split#1(nil())] = [4] [0] > [2] [0] = [nil()] [splitqs#1(::(@x, @xs), @pivot)] = [0 0] @pivot + [1 0] @x + [1 3] @xs + [3] [2 0] [2 0] [2 4] [2] >= [0 0] @pivot + [1 0] @x + [1 2] @xs + [3] [2 0] [2 0] [2 4] [2] = [splitqs#2(splitqs(@pivot, @xs), @pivot, @x)] [splitqs#1(nil(), @pivot)] = [0 0] @pivot + [3] [2 0] [4] > [0] [0] = [tuple#2(nil(), nil())] [splitqs#2(tuple#2(@ls, @rs), @pivot, @x)] = [0 1] @ls + [0 0] @pivot + [1 0] @x + [2] [0 2] [2 0] [2 0] [0] >= [0 1] @ls + [0 0] @pivot + [0 0] @x + [2] [0 1] [2 0] [2 0] [0] = [splitqs#3(#greater(@x, @pivot), @ls, @rs, @x)] [splitqs#3(#false(), @ls, @rs, @x)] = [0 1] @ls + [2] [0 1] [2] > [0 1] @ls + [1] [0 1] [1] = [tuple#2(::(@x, @ls), @rs)] [splitqs#3(#true(), @ls, @rs, @x)] = [0 1] @ls + [2] [0 1] [0] > [0 1] @ls + [0] [0 1] [0] = [tuple#2(@ls, ::(@x, @rs))] [#and(#false(), #false())] = [1] [2] >= [1] [1] = [#false()] [#and(#false(), #true())] = [1] [2] >= [1] [1] = [#false()] [#and(#true(), #false())] = [1] [2] >= [1] [1] = [#false()] [#and(#true(), #true())] = [1] [2] > [0] [1] = [#true()] [append^#(@l, @ys)] = [0] [0] >= [0] [0] = [c_1(append#1^#(@l, @ys))] [append#1^#(::(@x, @xs), @ys)] = [0] [0] >= [0] [0] = [c_2(append^#(@xs, @ys))] [insert^#(@x, @l)] = [0 1] @l + [0] [0 0] [1] >= [0 1] @l + [0] [0 0] [0] = [c_3(insert#1^#(@x, @l, @x))] [insert#1^#(tuple#2(@valX, @keyX), @l, @x)] = [0 1] @l + [0] [0 0] [0] >= [0 1] @l + [0] [0 0] [0] = [c_4(insert#2^#(@l, @keyX, @valX, @x))] [insert#2^#(::(@l1, @ls), @keyX, @valX, @x)] = [0 0] @keyX + [0 1] @ls + [1] [1 1] [0 0] [0] >= [0 1] @ls + [1] [0 0] [0] = [c_5(insert#3^#(@l1, @keyX, @ls, @valX, @x))] [insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x)] = [0 1] @ls + [1] [0 0] [1] > [0 1] @ls + [0] [0 0] [0] = [c_6(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x))] [insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x)] = [0 1] @ls + [0] [0 0] [0] >= [0 1] @ls + [0] [0 0] [0] = [c_7(insert^#(@x, @ls))] [quicksort^#(@l)] = [0] [0] >= [0] [0] = [c_8(quicksort#1^#(@l))] [quicksort#1^#(::(@z, @zs))] = [0] [0] >= [0] [0] = [c_9(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs))] [quicksort#2^#(tuple#2(@xs, @ys), @z)] = [0] [0] >= [0] [0] = [c_10(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys))] [splitqs^#(@pivot, @l)] = [0] [0] >= [0] [0] = [c_11(splitqs#1^#(@l, @pivot))] [splitqs#1^#(::(@x, @xs), @pivot)] = [0] [0] >= [0] [0] = [c_12(splitqs^#(@pivot, @xs))] [sortAll^#(@l)] = [2] [0] >= [2] [0] = [c_13(sortAll#1^#(@l))] [sortAll#1^#(::(@x, @xs))] = [2] [0] >= [2] [0] = [c_14(sortAll#2^#(@x, @xs))] [sortAll#2^#(tuple#2(@vals, @key), @xs)] = [0 0] @vals + [0 0] @xs + [2] [0 1] [1 1] [0] >= [2] [0] = [c_15(quicksort^#(@vals), sortAll^#(@xs))] [split^#(@l)] = [1 1] @l + [0] [0 1] [0] >= [1 1] @l + [0] [0 0] [0] = [c_16(split#1^#(@l))] [split#1^#(::(@x, @xs))] = [1 0] @x + [1 2] @xs + [1] [0 0] [0 0] [0] >= [1 2] @xs + [1] [0 0] [0] = [c_17(insert^#(@x, split(@xs)), split^#(@xs))] [splitAndSort^#(@l)] = [2 2] @l + [2] [1 2] [1] >= [2 2] @l + [2] [0 0] [1] = [c_18(sortAll^#(split(@l)), split^#(@l))] Consider the set of all dependency pairs DPs: { 1: append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , 2: append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , 3: insert^#(@x, @l) -> c_3(insert#1^#(@x, @l, @x)) , 4: insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_4(insert#2^#(@l, @keyX, @valX, @x)) , 5: insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_5(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , 6: insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_6(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)) , 7: insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_7(insert^#(@x, @ls)) , 8: quicksort^#(@l) -> c_8(quicksort#1^#(@l)) , 9: quicksort#1^#(::(@z, @zs)) -> c_9(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , 10: quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_10(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , 11: splitqs^#(@pivot, @l) -> c_11(splitqs#1^#(@l, @pivot)) , 12: splitqs#1^#(::(@x, @xs), @pivot) -> c_12(splitqs^#(@pivot, @xs)) , 13: sortAll^#(@l) -> c_13(sortAll#1^#(@l)) , 14: sortAll#1^#(::(@x, @xs)) -> c_14(sortAll#2^#(@x, @xs)) , 15: sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_15(quicksort^#(@vals), sortAll^#(@xs)) , 16: split^#(@l) -> c_16(split#1^#(@l)) , 17: split#1^#(::(@x, @xs)) -> c_17(insert^#(@x, split(@xs)), split^#(@xs)) , 18: splitAndSort^#(@l) -> c_18(sortAll^#(split(@l)), split^#(@l)) } Processor 'matrix interpretation of dimension 2' induces the complexity certificate YES(?,O(n^2)) on application of dependency pairs {6}. These cover all (indirect) predecessors of dependency pairs {6,7,18}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , insert^#(@x, @l) -> c_3(insert#1^#(@x, @l, @x)) , insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_4(insert#2^#(@l, @keyX, @valX, @x)) , insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_5(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , quicksort^#(@l) -> c_8(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_9(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_10(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_11(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_12(splitqs^#(@pivot, @xs)) , sortAll^#(@l) -> c_13(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_14(sortAll#2^#(@x, @xs)) , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_15(quicksort^#(@vals), sortAll^#(@xs)) , split^#(@l) -> c_16(split#1^#(@l)) , split#1^#(::(@x, @xs)) -> c_17(insert^#(@x, split(@xs)), split^#(@xs)) } Weak DPs: { insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_6(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)) , insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_7(insert^#(@x, @ls)) , splitAndSort^#(@l) -> c_18(sortAll^#(split(@l)), split^#(@l)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. DPs: { 5: insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_5(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , 13: sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_15(quicksort^#(@vals), sortAll^#(@xs)) , 15: split#1^#(::(@x, @xs)) -> c_17(insert^#(@x, split(@xs)), split^#(@xs)) } Trs: { #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append#1(nil(), @ys) -> @ys , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1, 2}, Uargs(c_10) = {1, 2, 3}, Uargs(c_11) = {1}, Uargs(c_12) = {1}, Uargs(c_13) = {1}, Uargs(c_14) = {1}, Uargs(c_15) = {1, 2}, Uargs(c_16) = {1}, Uargs(c_17) = {1, 2}, Uargs(c_18) = {1, 2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#equal](x1, x2) = [0 1] x2 + [1] [0 0] [0] [#eq](x1, x2) = [0 1] x2 + [1] [0 0] [0] [#greater](x1, x2) = [2] [0] [#compare](x1, x2) = [1] [0] [#ckgt](x1) = [2 2] x1 + [0] [0 0] [0] [append](x1, x2) = [1 0] x1 + [0] [0 0] [0] [append#1](x1, x2) = [1 0] x1 + [2 0] x2 + [0] [0 0] [0 2] [0] [::](x1, x2) = [1 0] x2 + [1] [1 1] [0] [nil] = [2] [0] [insert](x1, x2) = [1 0] x2 + [1] [1 1] [0] [insert#1](x1, x2, x3) = [1 0] x2 + [1] [1 1] [0] [tuple#2](x1, x2) = [0 0] x1 + [2] [1 0] [2] [insert#2](x1, x2, x3, x4) = [1 0] x1 + [1] [1 1] [0] [insert#3](x1, x2, x3, x4, x5) = [1 0] x3 + [2] [2 1] [1] [insert#4](x1, x2, x3, x4, x5, x6) = [0 0] x1 + [1 0] x3 + [2] [0 1] [2 1] [1] [#false] = [1] [0] [#true] = [1] [0] [quicksort](x1) = [0 0] x1 + [0] [2 1] [2] [quicksort#1](x1) = [0 0] x1 + [0] [2 0] [2] [splitqs](x1, x2) = [1 0] x2 + [1] [2 2] [1] [quicksort#2](x1, x2) = [2 1] x1 + [0 0] x2 + [0] [2 0] [0 1] [0] [sortAll](x1) = [0] [0] [sortAll#1](x1) = [0] [0] [sortAll#2](x1, x2) = [0] [0] [split](x1) = [1 0] x1 + [0] [1 1] [0] [split#1](x1) = [1 0] x1 + [0] [1 1] [0] [splitAndSort](x1) = [0] [0] [splitqs#1](x1, x2) = [1 0] x1 + [0] [2 2] [1] [splitqs#2](x1, x2, x3) = [1 0] x1 + [0] [1 1] [1] [splitqs#3](x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [2] [2 0] [1 0] [1] [#and](x1, x2) = [1] [0] [#EQ] = [1] [0] [#GT] = [1] [0] [#LT] = [1] [0] [#0] = [1] [0] [#neg](x1) = [1 0] x1 + [0] [0 1] [0] [#pos](x1) = [1 0] x1 + [0] [0 1] [0] [#s](x1) = [1 0] x1 + [0] [0 1] [0] [#equal^#](x1, x2) = [0] [0] [c_1](x1) = [0] [0] [#eq^#](x1, x2) = [0] [0] [#greater^#](x1, x2) = [0] [0] [c_2](x1, x2) = [0] [0] [#ckgt^#](x1) = [0] [0] [#compare^#](x1, x2) = [0] [0] [append^#](x1, x2) = [0] [0] [c_3](x1) = [0] [0] [append#1^#](x1, x2) = [0] [0] [c_4](x1) = [0] [0] [c_5] = [0] [0] [insert^#](x1, x2) = [1 0] x2 + [0] [1 1] [0] [c_6](x1) = [0] [0] [insert#1^#](x1, x2, x3) = [1 0] x2 + [0] [0 0] [0] [c_7](x1) = [0] [0] [insert#2^#](x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0] [0 0] [1 1] [1] [c_8](x1) = [0] [0] [insert#3^#](x1, x2, x3, x4, x5) = [1 0] x3 + [0] [0 0] [0] [c_9] = [0] [0] [c_10](x1, x2) = [0] [0] [insert#4^#](x1, x2, x3, x4, x5, x6) = [0 0] x1 + [1 0] x3 + [0] [2 0] [0 0] [1] [c_11](x1) = [0] [0] [c_12] = [0] [0] [quicksort^#](x1) = [0 0] x1 + [0] [1 1] [1] [c_13](x1) = [0] [0] [quicksort#1^#](x1) = [0] [0] [c_14](x1, x2) = [0] [0] [quicksort#2^#](x1, x2) = [0 0] x1 + [0] [2 0] [1] [splitqs^#](x1, x2) = [0 0] x2 + [0] [0 1] [0] [c_15] = [0] [0] [c_16](x1) = [0] [0] [splitqs#1^#](x1, x2) = [0] [0] [c_17](x1, x2, x3) = [0] [0] [sortAll^#](x1) = [1 0] x1 + [0] [0 0] [0] [c_18](x1) = [0] [0] [sortAll#1^#](x1) = [1 0] x1 + [0] [0 0] [0] [c_19](x1) = [0] [0] [sortAll#2^#](x1, x2) = [1 0] x2 + [1] [1 1] [0] [c_20] = [0] [0] [c_21](x1, x2) = [0] [0] [split^#](x1) = [1 2] x1 + [0] [1 1] [0] [c_22](x1) = [0] [0] [split#1^#](x1) = [1 2] x1 + [0] [0 0] [0] [c_23](x1, x2) = [0] [0] [c_24] = [0] [0] [splitAndSort^#](x1) = [2 2] x1 + [1] [2 1] [1] [c_25](x1, x2) = [0] [0] [c_26](x1, x2) = [0] [0] [splitqs#2^#](x1, x2, x3) = [0] [0] [c_27] = [0] [0] [c_28](x1, x2) = [0] [0] [splitqs#3^#](x1, x2, x3, x4) = [0] [0] [c_29] = [0] [0] [c_30] = [0] [0] [c_31](x1, x2, x3) = [0] [0] [#and^#](x1, x2) = [0] [0] [c_32] = [0] [0] [c_33] = [0] [0] [c_34] = [0] [0] [c_35] = [0] [0] [c_36] = [0] [0] [c_37] = [0] [0] [c_38] = [0] [0] [c_39](x1, x2, x3) = [0] [0] [c_40] = [0] [0] [c_41] = [0] [0] [c_42] = [0] [0] [c_43] = [0] [0] [c_44] = [0] [0] [c_45](x1) = [0] [0] [c_46] = [0] [0] [c_47] = [0] [0] [c_48] = [0] [0] [c_49](x1) = [0] [0] [c_50] = [0] [0] [c_51](x1) = [0] [0] [c_52] = [0] [0] [c_53] = [0] [0] [c_54] = [0] [0] [c_55] = [0] [0] [c_56] = [0] [0] [c_57](x1) = [0] [0] [c_58] = [0] [0] [c_59] = [0] [0] [c_60] = [0] [0] [c_61](x1) = [0] [0] [c_62] = [0] [0] [c_63](x1) = [0] [0] [c_64] = [0] [0] [c_65] = [0] [0] [c_66] = [0] [0] [c_67] = [0] [0] [c_68] = [0] [0] [c_69] = [0] [0] [c_70] = [0] [0] [c] = [0] [0] [c_1](x1) = [1 0] x1 + [0] [0 0] [0] [c_2](x1) = [1 0] x1 + [0] [0 0] [0] [c_3](x1) = [1 0] x1 + [0] [0 0] [0] [c_4](x1) = [1 0] x1 + [0] [0 0] [0] [c_5](x1) = [1 0] x1 + [0] [0 0] [0] [c_6](x1) = [1 0] x1 + [0] [0 0] [0] [c_7](x1) = [1 0] x1 + [0] [0 0] [0] [c_8](x1) = [1 0] x1 + [0] [0 0] [0] [c_9](x1, x2) = [2 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [c_10](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [2 0] x3 + [0] [0 0] [0 0] [0 0] [0] [c_11](x1) = [1 0] x1 + [0] [0 0] [0] [c_12](x1) = [1 0] x1 + [0] [0 0] [0] [c_13](x1) = [1 0] x1 + [0] [0 0] [0] [c_14](x1) = [1 0] x1 + [0] [0 0] [0] [c_15](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [c_16](x1) = [1 0] x1 + [0] [0 0] [0] [c_17](x1, x2) = [2 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [c_18](x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [0] This order satisfies following ordering constraints [#equal(@x, @y)] = [0 1] @y + [1] [0 0] [0] >= [0 1] @y + [1] [0 0] [0] = [#eq(@x, @y)] [#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [1 1] @y_2 + [1] [0 0] [0] >= [1] [0] = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] [#eq(::(@x_1, @x_2), nil())] = [1] [0] >= [1] [0] = [#false()] [#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2))] = [1 0] @y_1 + [3] [0 0] [0] > [1] [0] = [#false()] [#eq(nil(), ::(@y_1, @y_2))] = [1 1] @y_2 + [1] [0 0] [0] >= [1] [0] = [#false()] [#eq(nil(), nil())] = [1] [0] >= [1] [0] = [#true()] [#eq(nil(), tuple#2(@y_1, @y_2))] = [1 0] @y_1 + [3] [0 0] [0] > [1] [0] = [#false()] [#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2))] = [1 1] @y_2 + [1] [0 0] [0] >= [1] [0] = [#false()] [#eq(tuple#2(@x_1, @x_2), nil())] = [1] [0] >= [1] [0] = [#false()] [#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2))] = [1 0] @y_1 + [3] [0 0] [0] > [1] [0] = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] [#eq(#0(), #0())] = [1] [0] >= [1] [0] = [#true()] [#eq(#0(), #neg(@y))] = [0 1] @y + [1] [0 0] [0] >= [1] [0] = [#false()] [#eq(#0(), #pos(@y))] = [0 1] @y + [1] [0 0] [0] >= [1] [0] = [#false()] [#eq(#0(), #s(@y))] = [0 1] @y + [1] [0 0] [0] >= [1] [0] = [#false()] [#eq(#neg(@x), #0())] = [1] [0] >= [1] [0] = [#false()] [#eq(#neg(@x), #neg(@y))] = [0 1] @y + [1] [0 0] [0] >= [0 1] @y + [1] [0 0] [0] = [#eq(@x, @y)] [#eq(#neg(@x), #pos(@y))] = [0 1] @y + [1] [0 0] [0] >= [1] [0] = [#false()] [#eq(#pos(@x), #0())] = [1] [0] >= [1] [0] = [#false()] [#eq(#pos(@x), #neg(@y))] = [0 1] @y + [1] [0 0] [0] >= [1] [0] = [#false()] [#eq(#pos(@x), #pos(@y))] = [0 1] @y + [1] [0 0] [0] >= [0 1] @y + [1] [0 0] [0] = [#eq(@x, @y)] [#eq(#s(@x), #0())] = [1] [0] >= [1] [0] = [#false()] [#eq(#s(@x), #s(@y))] = [0 1] @y + [1] [0 0] [0] >= [0 1] @y + [1] [0 0] [0] = [#eq(@x, @y)] [#greater(@x, @y)] = [2] [0] >= [2] [0] = [#ckgt(#compare(@x, @y))] [#compare(#0(), #0())] = [1] [0] >= [1] [0] = [#EQ()] [#compare(#0(), #neg(@y))] = [1] [0] >= [1] [0] = [#GT()] [#compare(#0(), #pos(@y))] = [1] [0] >= [1] [0] = [#LT()] [#compare(#0(), #s(@y))] = [1] [0] >= [1] [0] = [#LT()] [#compare(#neg(@x), #0())] = [1] [0] >= [1] [0] = [#LT()] [#compare(#neg(@x), #neg(@y))] = [1] [0] >= [1] [0] = [#compare(@y, @x)] [#compare(#neg(@x), #pos(@y))] = [1] [0] >= [1] [0] = [#LT()] [#compare(#pos(@x), #0())] = [1] [0] >= [1] [0] = [#GT()] [#compare(#pos(@x), #neg(@y))] = [1] [0] >= [1] [0] = [#GT()] [#compare(#pos(@x), #pos(@y))] = [1] [0] >= [1] [0] = [#compare(@x, @y)] [#compare(#s(@x), #0())] = [1] [0] >= [1] [0] = [#GT()] [#compare(#s(@x), #s(@y))] = [1] [0] >= [1] [0] = [#compare(@x, @y)] [#ckgt(#EQ())] = [2] [0] > [1] [0] = [#false()] [#ckgt(#GT())] = [2] [0] > [1] [0] = [#true()] [#ckgt(#LT())] = [2] [0] > [1] [0] = [#false()] [insert(@x, @l)] = [1 0] @l + [1] [1 1] [0] >= [1 0] @l + [1] [1 1] [0] = [insert#1(@x, @l, @x)] [insert#1(tuple#2(@valX, @keyX), @l, @x)] = [1 0] @l + [1] [1 1] [0] >= [1 0] @l + [1] [1 1] [0] = [insert#2(@l, @keyX, @valX, @x)] [insert#2(::(@l1, @ls), @keyX, @valX, @x)] = [1 0] @ls + [2] [2 1] [1] >= [1 0] @ls + [2] [2 1] [1] = [insert#3(@l1, @keyX, @ls, @valX, @x)] [insert#2(nil(), @keyX, @valX, @x)] = [3] [2] >= [3] [2] = [::(tuple#2(::(@valX, nil()), @keyX), nil())] [insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x)] = [1 0] @ls + [2] [2 1] [1] >= [1 0] @ls + [2] [2 1] [1] = [insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)] [insert#4(#false(), @key1, @ls, @valX, @vals1, @x)] = [1 0] @ls + [2] [2 1] [1] >= [1 0] @ls + [2] [2 1] [1] = [::(tuple#2(@vals1, @key1), insert(@x, @ls))] [insert#4(#true(), @key1, @ls, @valX, @vals1, @x)] = [1 0] @ls + [2] [2 1] [1] > [1 0] @ls + [1] [1 1] [0] = [::(tuple#2(::(@valX, @vals1), @key1), @ls)] [splitqs(@pivot, @l)] = [1 0] @l + [1] [2 2] [1] > [1 0] @l + [0] [2 2] [1] = [splitqs#1(@l, @pivot)] [split(@l)] = [1 0] @l + [0] [1 1] [0] >= [1 0] @l + [0] [1 1] [0] = [split#1(@l)] [split#1(::(@x, @xs))] = [1 0] @xs + [1] [2 1] [1] >= [1 0] @xs + [1] [2 1] [0] = [insert(@x, split(@xs))] [split#1(nil())] = [2] [2] >= [2] [0] = [nil()] [splitqs#1(::(@x, @xs), @pivot)] = [1 0] @xs + [1] [4 2] [3] >= [1 0] @xs + [1] [3 2] [3] = [splitqs#2(splitqs(@pivot, @xs), @pivot, @x)] [splitqs#1(nil(), @pivot)] = [2] [5] >= [2] [4] = [tuple#2(nil(), nil())] [splitqs#2(tuple#2(@ls, @rs), @pivot, @x)] = [0 0] @ls + [2] [1 0] [5] >= [0 0] @ls + [2] [1 0] [5] = [splitqs#3(#greater(@x, @pivot), @ls, @rs, @x)] [splitqs#3(#false(), @ls, @rs, @x)] = [0 0] @ls + [2] [1 0] [3] >= [0 0] @ls + [2] [1 0] [3] = [tuple#2(::(@x, @ls), @rs)] [splitqs#3(#true(), @ls, @rs, @x)] = [0 0] @ls + [2] [1 0] [3] >= [0 0] @ls + [2] [1 0] [2] = [tuple#2(@ls, ::(@x, @rs))] [#and(#false(), #false())] = [1] [0] >= [1] [0] = [#false()] [#and(#false(), #true())] = [1] [0] >= [1] [0] = [#false()] [#and(#true(), #false())] = [1] [0] >= [1] [0] = [#false()] [#and(#true(), #true())] = [1] [0] >= [1] [0] = [#true()] [append^#(@l, @ys)] = [0] [0] >= [0] [0] = [c_1(append#1^#(@l, @ys))] [append#1^#(::(@x, @xs), @ys)] = [0] [0] >= [0] [0] = [c_2(append^#(@xs, @ys))] [insert^#(@x, @l)] = [1 0] @l + [0] [1 1] [0] >= [1 0] @l + [0] [0 0] [0] = [c_3(insert#1^#(@x, @l, @x))] [insert#1^#(tuple#2(@valX, @keyX), @l, @x)] = [1 0] @l + [0] [0 0] [0] >= [1 0] @l + [0] [0 0] [0] = [c_4(insert#2^#(@l, @keyX, @valX, @x))] [insert#2^#(::(@l1, @ls), @keyX, @valX, @x)] = [0 0] @keyX + [1 0] @ls + [1] [1 1] [0 0] [1] > [1 0] @ls + [0] [0 0] [0] = [c_5(insert#3^#(@l1, @keyX, @ls, @valX, @x))] [insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x)] = [1 0] @ls + [0] [0 0] [0] >= [1 0] @ls + [0] [0 0] [0] = [c_6(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x))] [insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x)] = [1 0] @ls + [0] [0 0] [3] >= [1 0] @ls + [0] [0 0] [0] = [c_7(insert^#(@x, @ls))] [quicksort^#(@l)] = [0 0] @l + [0] [1 1] [1] >= [0] [0] = [c_8(quicksort#1^#(@l))] [quicksort#1^#(::(@z, @zs))] = [0] [0] >= [0] [0] = [c_9(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs))] [quicksort#2^#(tuple#2(@xs, @ys), @z)] = [0] [5] >= [0] [0] = [c_10(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys))] [splitqs^#(@pivot, @l)] = [0 0] @l + [0] [0 1] [0] >= [0] [0] = [c_11(splitqs#1^#(@l, @pivot))] [splitqs#1^#(::(@x, @xs), @pivot)] = [0] [0] >= [0] [0] = [c_12(splitqs^#(@pivot, @xs))] [sortAll^#(@l)] = [1 0] @l + [0] [0 0] [0] >= [1 0] @l + [0] [0 0] [0] = [c_13(sortAll#1^#(@l))] [sortAll#1^#(::(@x, @xs))] = [1 0] @xs + [1] [0 0] [0] >= [1 0] @xs + [1] [0 0] [0] = [c_14(sortAll#2^#(@x, @xs))] [sortAll#2^#(tuple#2(@vals, @key), @xs)] = [1 0] @xs + [1] [1 1] [0] > [1 0] @xs + [0] [0 0] [0] = [c_15(quicksort^#(@vals), sortAll^#(@xs))] [split^#(@l)] = [1 2] @l + [0] [1 1] [0] >= [1 2] @l + [0] [0 0] [0] = [c_16(split#1^#(@l))] [split#1^#(::(@x, @xs))] = [3 2] @xs + [1] [0 0] [0] > [3 2] @xs + [0] [0 0] [0] = [c_17(insert^#(@x, split(@xs)), split^#(@xs))] [splitAndSort^#(@l)] = [2 2] @l + [1] [2 1] [1] >= [2 2] @l + [1] [0 0] [0] = [c_18(sortAll^#(split(@l)), split^#(@l))] Consider the set of all dependency pairs DPs: { 1: append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , 2: append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , 3: insert^#(@x, @l) -> c_3(insert#1^#(@x, @l, @x)) , 4: insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_4(insert#2^#(@l, @keyX, @valX, @x)) , 5: insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_5(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , 6: quicksort^#(@l) -> c_8(quicksort#1^#(@l)) , 7: quicksort#1^#(::(@z, @zs)) -> c_9(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , 8: quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_10(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , 9: splitqs^#(@pivot, @l) -> c_11(splitqs#1^#(@l, @pivot)) , 10: splitqs#1^#(::(@x, @xs), @pivot) -> c_12(splitqs^#(@pivot, @xs)) , 11: sortAll^#(@l) -> c_13(sortAll#1^#(@l)) , 12: sortAll#1^#(::(@x, @xs)) -> c_14(sortAll#2^#(@x, @xs)) , 13: sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_15(quicksort^#(@vals), sortAll^#(@xs)) , 14: split^#(@l) -> c_16(split#1^#(@l)) , 15: split#1^#(::(@x, @xs)) -> c_17(insert^#(@x, split(@xs)), split^#(@xs)) , 16: insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_6(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)) , 17: insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_7(insert^#(@x, @ls)) , 18: splitAndSort^#(@l) -> c_18(sortAll^#(split(@l)), split^#(@l)) } Processor 'matrix interpretation of dimension 2' induces the complexity certificate YES(?,O(n^2)) on application of dependency pairs {5,13,15}. These cover all (indirect) predecessors of dependency pairs {3,4,5,11,12,13,14,15,16,17,18}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_8(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_9(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_10(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_11(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_12(splitqs^#(@pivot, @xs)) } Weak DPs: { insert^#(@x, @l) -> c_3(insert#1^#(@x, @l, @x)) , insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_4(insert#2^#(@l, @keyX, @valX, @x)) , insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_5(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_6(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)) , insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_7(insert^#(@x, @ls)) , sortAll^#(@l) -> c_13(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_14(sortAll#2^#(@x, @xs)) , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_15(quicksort^#(@vals), sortAll^#(@xs)) , split^#(@l) -> c_16(split#1^#(@l)) , split#1^#(::(@x, @xs)) -> c_17(insert^#(@x, split(@xs)), split^#(@xs)) , splitAndSort^#(@l) -> c_18(sortAll^#(split(@l)), split^#(@l)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { insert^#(@x, @l) -> c_3(insert#1^#(@x, @l, @x)) , insert#1^#(tuple#2(@valX, @keyX), @l, @x) -> c_4(insert#2^#(@l, @keyX, @valX, @x)) , insert#2^#(::(@l1, @ls), @keyX, @valX, @x) -> c_5(insert#3^#(@l1, @keyX, @ls, @valX, @x)) , insert#3^#(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> c_6(insert#4^#(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)) , insert#4^#(#false(), @key1, @ls, @valX, @vals1, @x) -> c_7(insert^#(@x, @ls)) , split^#(@l) -> c_16(split#1^#(@l)) , split#1^#(::(@x, @xs)) -> c_17(insert^#(@x, split(@xs)), split^#(@xs)) } We apply the transformation 'simpDPRHS' on the sub-problem: Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_8(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_9(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_10(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_11(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_12(splitqs^#(@pivot, @xs)) } Weak DPs: { sortAll^#(@l) -> c_13(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_14(sortAll#2^#(@x, @xs)) , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_15(quicksort^#(@vals), sortAll^#(@xs)) , splitAndSort^#(@l) -> c_18(sortAll^#(split(@l)), split^#(@l)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } StartTerms: basic terms Strategy: innermost Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { splitAndSort^#(@l) -> c_18(sortAll^#(split(@l)), split^#(@l)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_3(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_4(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_5(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , splitqs^#(@pivot, @l) -> c_6(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_7(splitqs^#(@pivot, @xs)) } Weak DPs: { sortAll^#(@l) -> c_8(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_9(sortAll#2^#(@x, @xs)) , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_10(quicksort^#(@vals), sortAll^#(@xs)) , splitAndSort^#(@l) -> c_11(sortAll^#(split(@l))) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'trivial' failed due to the following reason: We use the processor 'matrix interpretation of dimension 3' to orient following rules strictly. DPs: { 4: quicksort#1^#(::(@z, @zs)) -> c_4(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) } Trs: { #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort#1(nil()) -> nil() , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1, 2, 3}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1, 2}, Uargs(c_11) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [0 0 0] [0] [#equal](x1, x2) = [1 1 0] x1 + [1] [0 0 1] [0] [0 0 0] [0] [#eq](x1, x2) = [1 1 0] x1 + [1] [0 0 0] [0] [0 1 0] [1 0 0] [1] [#greater](x1, x2) = [1 0 0] x1 + [1 1 0] x2 + [0] [0 0 0] [1 0 0] [0] [0 0 0] [0 0 0] [0] [#compare](x1, x2) = [1 0 0] x1 + [0 1 0] x2 + [0] [0 0 0] [0 0 0] [1] [1 0 0] [1] [#ckgt](x1) = [1 1 0] x1 + [0] [1 0 0] [0] [0 0 0] [1 0 0] [0] [append](x1, x2) = [0 0 1] x1 + [0 1 1] x2 + [0] [0 0 1] [0 1 1] [0] [1 0 0] [1 0 0] [0] [append#1](x1, x2) = [0 1 0] x1 + [0 1 0] x2 + [0] [0 0 0] [0 0 1] [0] [0 0 0] [1 1 0] [0] [::](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [1] [1 0 0] [0 0 1] [0] [0] [nil] = [0] [1] [0 0 0] [1 1 0] [0] [insert](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [1] [1 0 0] [0 0 1] [1] [1 1 0] [0 0 0] [0] [insert#1](x1, x2, x3) = [0 0 0] x2 + [0 0 0] x3 + [1] [0 0 1] [1 0 0] [1] [1 1 0] [0 0 0] [0] [tuple#2](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [1 1 0] [1 1 0] [0] [1 1 0] [0 0 0] [0] [insert#2](x1, x2, x3, x4) = [0 0 0] x1 + [0 0 0] x4 + [1] [0 0 1] [1 0 0] [1] [0 0 0] [1 1 0] [0 0 0] [1] [insert#3](x1, x2, x3, x4, x5) = [0 0 0] x1 + [0 0 0] x3 + [0 0 0] x5 + [1] [1 0 0] [0 0 1] [1 0 0] [1] [1 0 0] [1 1 0] [0 0 0] [0 0 0] [1] [insert#4](x1, x2, x3, x4, x5, x6) = [0 0 0] x1 + [0 0 0] x3 + [0 0 0] x5 + [0 0 0] x6 + [1] [0 0 0] [0 0 1] [1 1 0] [1 0 0] [1] [0] [#false] = [1] [0] [0] [#true] = [1] [0] [0 1 0] [1] [quicksort](x1) = [1 0 0] x1 + [0] [0 0 0] [1] [0 0 0] [1] [quicksort#1](x1) = [0 0 0] x1 + [0] [1 0 1] [0] [1 0 0] [1 1 0] [0] [splitqs](x1, x2) = [1 1 0] x1 + [1 1 1] x2 + [0] [0 0 0] [1 1 0] [0] [0 0 1] [0 0 0] [1] [quicksort#2](x1, x2) = [0 0 1] x1 + [0 0 0] x2 + [0] [0 0 0] [1 0 0] [1] [1 1 0] [0] [split](x1) = [0 0 0] x1 + [1] [1 1 1] [1] [1 1 0] [0] [split#1](x1) = [0 0 0] x1 + [1] [1 1 1] [1] [1 1 0] [1 0 0] [0] [splitqs#1](x1, x2) = [1 1 1] x1 + [1 1 0] x2 + [0] [1 1 0] [0 0 0] [0] [1 0 0] [0 0 0] [0 0 0] [1] [splitqs#2](x1, x2, x3) = [0 0 1] x1 + [1 1 0] x2 + [1 0 0] x3 + [0] [0 0 1] [0 0 0] [0 0 0] [1] [0 0 0] [1 1 0] [0 0 0] [1] [splitqs#3](x1, x2, x3, x4) = [0 1 0] x1 + [1 1 0] x2 + [1 1 0] x3 + [0] [0 0 0] [1 1 0] [1 1 0] [1] [0] [#and](x1, x2) = [1] [0] [0] [#EQ] = [1] [0] [0] [#GT] = [1] [1] [0] [#LT] = [1] [1] [1] [#0] = [0] [1] [0 1 0] [1] [#neg](x1) = [1 0 0] x1 + [0] [1 1 1] [1] [1 0 0] [1] [#pos](x1) = [0 1 0] x1 + [0] [1 1 1] [0] [1 0 0] [1] [#s](x1) = [0 1 0] x1 + [0] [1 0 1] [0] [0] [#equal^#](x1, x2) = [0] [0] [0] [#eq^#](x1, x2) = [0] [0] [0] [#greater^#](x1, x2) = [0] [0] [0] [#ckgt^#](x1) = [0] [0] [0] [#compare^#](x1, x2) = [0] [0] [0] [append^#](x1, x2) = [0] [0] [0] [append#1^#](x1, x2) = [0] [0] [0] [insert^#](x1, x2) = [0] [0] [0] [insert#1^#](x1, x2, x3) = [0] [0] [0] [insert#2^#](x1, x2, x3, x4) = [0] [0] [0] [insert#3^#](x1, x2, x3, x4, x5) = [0] [0] [0] [insert#4^#](x1, x2, x3, x4, x5, x6) = [0] [0] [1 1 0] [0] [quicksort^#](x1) = [0 0 0] x1 + [1] [1 0 0] [0] [1 1 0] [0] [quicksort#1^#](x1) = [0 0 0] x1 + [1] [0 0 0] [0] [0 0 1] [0] [quicksort#2^#](x1, x2) = [0 0 0] x1 + [1] [0 0 0] [0] [0] [splitqs^#](x1, x2) = [1] [1] [0] [splitqs#1^#](x1, x2) = [0] [0] [0 0 1] [0] [sortAll^#](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [0 0 1] [0] [sortAll#1^#](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0 0 1] [0] [sortAll#2^#](x1, x2) = [1 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [0] [split^#](x1) = [0] [0] [0] [split#1^#](x1) = [0] [0] [1 1 1] [1] [splitAndSort^#](x1) = [1 1 1] x1 + [1] [1 1 1] [1] [0] [splitqs#2^#](x1, x2, x3) = [0] [0] [0] [splitqs#3^#](x1, x2, x3, x4) = [0] [0] [0] [#and^#](x1, x2) = [0] [0] [1 0 0] [0] [c_1](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_2](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_3](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [1 0 0] [0] [c_4](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [1 1 1] [1 0 0] [1 0 0] [0] [c_5](x1, x2, x3) = [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0] [0 0 0] [0 0 0] [0 0 0] [0] [1 0 0] [0] [c_6](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_7](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_8](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [0] [c_9](x1) = [0 0 0] x1 + [0] [0 0 0] [0] [1 0 0] [1 0 0] [0] [c_10](x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 0] [0] [1 0 0] [0] [c_11](x1) = [0 0 0] x1 + [0] [0 0 0] [0] This order satisfies following ordering constraints [#equal(@x, @y)] = [0 0 0] [0] [1 1 0] @x + [1] [0 0 1] [0] >= [0 0 0] [0] [1 1 0] @x + [1] [0 0 0] [0] = [#eq(@x, @y)] [#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [0 0 0] [0] [1 1 0] @x_2 + [2] [0 0 0] [0] >= [0] [1] [0] = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] [#eq(::(@x_1, @x_2), nil())] = [0 0 0] [0] [1 1 0] @x_2 + [2] [0 0 0] [0] >= [0] [1] [0] = [#false()] [#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2))] = [0 0 0] [0] [1 1 0] @x_2 + [2] [0 0 0] [0] >= [0] [1] [0] = [#false()] [#eq(nil(), ::(@y_1, @y_2))] = [0] [1] [0] >= [0] [1] [0] = [#false()] [#eq(nil(), nil())] = [0] [1] [0] >= [0] [1] [0] = [#true()] [#eq(nil(), tuple#2(@y_1, @y_2))] = [0] [1] [0] >= [0] [1] [0] = [#false()] [#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2))] = [0 0 0] [0] [1 1 0] @x_1 + [1] [0 0 0] [0] >= [0] [1] [0] = [#false()] [#eq(tuple#2(@x_1, @x_2), nil())] = [0 0 0] [0] [1 1 0] @x_1 + [1] [0 0 0] [0] >= [0] [1] [0] = [#false()] [#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2))] = [0 0 0] [0] [1 1 0] @x_1 + [1] [0 0 0] [0] >= [0] [1] [0] = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] [#eq(#0(), #0())] = [0] [2] [0] >= [0] [1] [0] = [#true()] [#eq(#0(), #neg(@y))] = [0] [2] [0] >= [0] [1] [0] = [#false()] [#eq(#0(), #pos(@y))] = [0] [2] [0] >= [0] [1] [0] = [#false()] [#eq(#0(), #s(@y))] = [0] [2] [0] >= [0] [1] [0] = [#false()] [#eq(#neg(@x), #0())] = [0 0 0] [0] [1 1 0] @x + [2] [0 0 0] [0] >= [0] [1] [0] = [#false()] [#eq(#neg(@x), #neg(@y))] = [0 0 0] [0] [1 1 0] @x + [2] [0 0 0] [0] >= [0 0 0] [0] [1 1 0] @x + [1] [0 0 0] [0] = [#eq(@x, @y)] [#eq(#neg(@x), #pos(@y))] = [0 0 0] [0] [1 1 0] @x + [2] [0 0 0] [0] >= [0] [1] [0] = [#false()] [#eq(#pos(@x), #0())] = [0 0 0] [0] [1 1 0] @x + [2] [0 0 0] [0] >= [0] [1] [0] = [#false()] [#eq(#pos(@x), #neg(@y))] = [0 0 0] [0] [1 1 0] @x + [2] [0 0 0] [0] >= [0] [1] [0] = [#false()] [#eq(#pos(@x), #pos(@y))] = [0 0 0] [0] [1 1 0] @x + [2] [0 0 0] [0] >= [0 0 0] [0] [1 1 0] @x + [1] [0 0 0] [0] = [#eq(@x, @y)] [#eq(#s(@x), #0())] = [0 0 0] [0] [1 1 0] @x + [2] [0 0 0] [0] >= [0] [1] [0] = [#false()] [#eq(#s(@x), #s(@y))] = [0 0 0] [0] [1 1 0] @x + [2] [0 0 0] [0] >= [0 0 0] [0] [1 1 0] @x + [1] [0 0 0] [0] = [#eq(@x, @y)] [#greater(@x, @y)] = [0 1 0] [1 0 0] [1] [1 0 0] @x + [1 1 0] @y + [0] [0 0 0] [1 0 0] [0] >= [0 0 0] [0 0 0] [1] [1 0 0] @x + [0 1 0] @y + [0] [0 0 0] [0 0 0] [0] = [#ckgt(#compare(@x, @y))] [#compare(#0(), #0())] = [0] [1] [1] >= [0] [1] [0] = [#EQ()] [#compare(#0(), #neg(@y))] = [0 0 0] [0] [1 0 0] @y + [1] [0 0 0] [1] >= [0] [1] [1] = [#GT()] [#compare(#0(), #pos(@y))] = [0 0 0] [0] [0 1 0] @y + [1] [0 0 0] [1] >= [0] [1] [1] = [#LT()] [#compare(#0(), #s(@y))] = [0 0 0] [0] [0 1 0] @y + [1] [0 0 0] [1] >= [0] [1] [1] = [#LT()] [#compare(#neg(@x), #0())] = [0 0 0] [0] [0 1 0] @x + [1] [0 0 0] [1] >= [0] [1] [1] = [#LT()] [#compare(#neg(@x), #neg(@y))] = [0 0 0] [0 0 0] [0] [0 1 0] @x + [1 0 0] @y + [1] [0 0 0] [0 0 0] [1] >= [0 0 0] [0 0 0] [0] [0 1 0] @x + [1 0 0] @y + [0] [0 0 0] [0 0 0] [1] = [#compare(@y, @x)] [#compare(#neg(@x), #pos(@y))] = [0 0 0] [0 0 0] [0] [0 1 0] @x + [0 1 0] @y + [1] [0 0 0] [0 0 0] [1] >= [0] [1] [1] = [#LT()] [#compare(#pos(@x), #0())] = [0 0 0] [0] [1 0 0] @x + [1] [0 0 0] [1] >= [0] [1] [1] = [#GT()] [#compare(#pos(@x), #neg(@y))] = [0 0 0] [0 0 0] [0] [1 0 0] @x + [1 0 0] @y + [1] [0 0 0] [0 0 0] [1] >= [0] [1] [1] = [#GT()] [#compare(#pos(@x), #pos(@y))] = [0 0 0] [0 0 0] [0] [1 0 0] @x + [0 1 0] @y + [1] [0 0 0] [0 0 0] [1] >= [0 0 0] [0 0 0] [0] [1 0 0] @x + [0 1 0] @y + [0] [0 0 0] [0 0 0] [1] = [#compare(@x, @y)] [#compare(#s(@x), #0())] = [0 0 0] [0] [1 0 0] @x + [1] [0 0 0] [1] >= [0] [1] [1] = [#GT()] [#compare(#s(@x), #s(@y))] = [0 0 0] [0 0 0] [0] [1 0 0] @x + [0 1 0] @y + [1] [0 0 0] [0 0 0] [1] >= [0 0 0] [0 0 0] [0] [1 0 0] @x + [0 1 0] @y + [0] [0 0 0] [0 0 0] [1] = [#compare(@x, @y)] [#ckgt(#EQ())] = [1] [1] [0] > [0] [1] [0] = [#false()] [#ckgt(#GT())] = [1] [1] [0] > [0] [1] [0] = [#true()] [#ckgt(#LT())] = [1] [1] [0] > [0] [1] [0] = [#false()] [insert(@x, @l)] = [1 1 0] [0 0 0] [0] [0 0 0] @l + [0 0 0] @x + [1] [0 0 1] [1 0 0] [1] >= [1 1 0] [0 0 0] [0] [0 0 0] @l + [0 0 0] @x + [1] [0 0 1] [1 0 0] [1] = [insert#1(@x, @l, @x)] [insert#1(tuple#2(@valX, @keyX), @l, @x)] = [1 1 0] [0 0 0] [0] [0 0 0] @l + [0 0 0] @x + [1] [0 0 1] [1 0 0] [1] >= [1 1 0] [0 0 0] [0] [0 0 0] @l + [0 0 0] @x + [1] [0 0 1] [1 0 0] [1] = [insert#2(@l, @keyX, @valX, @x)] [insert#2(::(@l1, @ls), @keyX, @valX, @x)] = [0 0 0] [1 1 0] [0 0 0] [1] [0 0 0] @l1 + [0 0 0] @ls + [0 0 0] @x + [1] [1 0 0] [0 0 1] [1 0 0] [1] >= [0 0 0] [1 1 0] [0 0 0] [1] [0 0 0] @l1 + [0 0 0] @ls + [0 0 0] @x + [1] [1 0 0] [0 0 1] [1 0 0] [1] = [insert#3(@l1, @keyX, @ls, @valX, @x)] [insert#2(nil(), @keyX, @valX, @x)] = [0 0 0] [0] [0 0 0] @x + [1] [1 0 0] [2] >= [0] [1] [2] = [::(tuple#2(::(@valX, nil()), @keyX), nil())] [insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x)] = [1 1 0] [0 0 0] [0 0 0] [1] [0 0 0] @ls + [0 0 0] @vals1 + [0 0 0] @x + [1] [0 0 1] [1 1 0] [1 0 0] [1] >= [1 1 0] [0 0 0] [0 0 0] [1] [0 0 0] @ls + [0 0 0] @vals1 + [0 0 0] @x + [1] [0 0 1] [1 1 0] [1 0 0] [1] = [insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)] [insert#4(#false(), @key1, @ls, @valX, @vals1, @x)] = [1 1 0] [0 0 0] [0 0 0] [1] [0 0 0] @ls + [0 0 0] @vals1 + [0 0 0] @x + [1] [0 0 1] [1 1 0] [1 0 0] [1] >= [1 1 0] [0 0 0] [0 0 0] [1] [0 0 0] @ls + [0 0 0] @vals1 + [0 0 0] @x + [1] [0 0 1] [1 1 0] [1 0 0] [1] = [::(tuple#2(@vals1, @key1), insert(@x, @ls))] [insert#4(#true(), @key1, @ls, @valX, @vals1, @x)] = [1 1 0] [0 0 0] [0 0 0] [1] [0 0 0] @ls + [0 0 0] @vals1 + [0 0 0] @x + [1] [0 0 1] [1 1 0] [1 0 0] [1] > [1 1 0] [0 0 0] [0] [0 0 0] @ls + [0 0 0] @vals1 + [1] [0 0 1] [1 1 0] [1] = [::(tuple#2(::(@valX, @vals1), @key1), @ls)] [splitqs(@pivot, @l)] = [1 1 0] [1 0 0] [0] [1 1 1] @l + [1 1 0] @pivot + [0] [1 1 0] [0 0 0] [0] >= [1 1 0] [1 0 0] [0] [1 1 1] @l + [1 1 0] @pivot + [0] [1 1 0] [0 0 0] [0] = [splitqs#1(@l, @pivot)] [split(@l)] = [1 1 0] [0] [0 0 0] @l + [1] [1 1 1] [1] >= [1 1 0] [0] [0 0 0] @l + [1] [1 1 1] [1] = [split#1(@l)] [split#1(::(@x, @xs))] = [0 0 0] [1 1 0] [1] [0 0 0] @x + [0 0 0] @xs + [1] [1 0 0] [1 1 1] [2] >= [0 0 0] [1 1 0] [1] [0 0 0] @x + [0 0 0] @xs + [1] [1 0 0] [1 1 1] [2] = [insert(@x, split(@xs))] [split#1(nil())] = [0] [1] [2] >= [0] [0] [1] = [nil()] [splitqs#1(::(@x, @xs), @pivot)] = [1 0 0] [0 0 0] [1 1 0] [1] [1 1 0] @pivot + [1 0 0] @x + [1 1 1] @xs + [1] [0 0 0] [0 0 0] [1 1 0] [1] >= [1 0 0] [0 0 0] [1 1 0] [1] [1 1 0] @pivot + [1 0 0] @x + [1 1 0] @xs + [0] [0 0 0] [0 0 0] [1 1 0] [1] = [splitqs#2(splitqs(@pivot, @xs), @pivot, @x)] [splitqs#1(nil(), @pivot)] = [1 0 0] [0] [1 1 0] @pivot + [1] [0 0 0] [0] >= [0] [0] [0] = [tuple#2(nil(), nil())] [splitqs#2(tuple#2(@ls, @rs), @pivot, @x)] = [1 1 0] [0 0 0] [0 0 0] [0 0 0] [1] [1 1 0] @ls + [1 1 0] @pivot + [1 1 0] @rs + [1 0 0] @x + [0] [1 1 0] [0 0 0] [1 1 0] [0 0 0] [1] >= [1 1 0] [0 0 0] [0 0 0] [0 0 0] [1] [1 1 0] @ls + [1 1 0] @pivot + [1 1 0] @rs + [1 0 0] @x + [0] [1 1 0] [0 0 0] [1 1 0] [0 0 0] [1] = [splitqs#3(#greater(@x, @pivot), @ls, @rs, @x)] [splitqs#3(#false(), @ls, @rs, @x)] = [1 1 0] [0 0 0] [1] [1 1 0] @ls + [1 1 0] @rs + [1] [1 1 0] [1 1 0] [1] >= [1 1 0] [0 0 0] [1] [0 0 0] @ls + [0 0 0] @rs + [0] [1 1 0] [1 1 0] [1] = [tuple#2(::(@x, @ls), @rs)] [splitqs#3(#true(), @ls, @rs, @x)] = [1 1 0] [0 0 0] [1] [1 1 0] @ls + [1 1 0] @rs + [1] [1 1 0] [1 1 0] [1] > [1 1 0] [0 0 0] [0] [0 0 0] @ls + [0 0 0] @rs + [0] [1 1 0] [1 1 0] [1] = [tuple#2(@ls, ::(@x, @rs))] [#and(#false(), #false())] = [0] [1] [0] >= [0] [1] [0] = [#false()] [#and(#false(), #true())] = [0] [1] [0] >= [0] [1] [0] = [#false()] [#and(#true(), #false())] = [0] [1] [0] >= [0] [1] [0] = [#false()] [#and(#true(), #true())] = [0] [1] [0] >= [0] [1] [0] = [#true()] [append^#(@l, @ys)] = [0] [0] [0] >= [0] [0] [0] = [c_1(append#1^#(@l, @ys))] [append#1^#(::(@x, @xs), @ys)] = [0] [0] [0] >= [0] [0] [0] = [c_2(append^#(@xs, @ys))] [quicksort^#(@l)] = [1 1 0] [0] [0 0 0] @l + [1] [1 0 0] [0] >= [1 1 0] [0] [0 0 0] @l + [0] [0 0 0] [0] = [c_3(quicksort#1^#(@l))] [quicksort#1^#(::(@z, @zs))] = [1 1 0] [1] [0 0 0] @zs + [1] [0 0 0] [0] > [1 1 0] [0] [0 0 0] @zs + [0] [0 0 0] [0] = [c_4(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs))] [quicksort#2^#(tuple#2(@xs, @ys), @z)] = [1 1 0] [1 1 0] [0] [0 0 0] @xs + [0 0 0] @ys + [1] [0 0 0] [0 0 0] [0] >= [1 1 0] [1 1 0] [0] [0 0 0] @xs + [0 0 0] @ys + [0] [0 0 0] [0 0 0] [0] = [c_5(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys))] [splitqs^#(@pivot, @l)] = [0] [1] [1] >= [0] [0] [0] = [c_6(splitqs#1^#(@l, @pivot))] [splitqs#1^#(::(@x, @xs), @pivot)] = [0] [0] [0] >= [0] [0] [0] = [c_7(splitqs^#(@pivot, @xs))] [sortAll^#(@l)] = [0 0 1] [0] [0 0 0] @l + [0] [0 0 0] [0] >= [0 0 1] [0] [0 0 0] @l + [0] [0 0 0] [0] = [c_8(sortAll#1^#(@l))] [sortAll#1^#(::(@x, @xs))] = [1 0 0] [0 0 1] [0] [0 0 0] @x + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0] >= [1 0 0] [0 0 1] [0] [0 0 0] @x + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0] = [c_9(sortAll#2^#(@x, @xs))] [sortAll#2^#(tuple#2(@vals, @key), @xs)] = [1 1 0] [0 0 1] [0] [1 1 0] @vals + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0] >= [1 1 0] [0 0 1] [0] [0 0 0] @vals + [0 0 0] @xs + [0] [0 0 0] [0 0 0] [0] = [c_10(quicksort^#(@vals), sortAll^#(@xs))] [splitAndSort^#(@l)] = [1 1 1] [1] [1 1 1] @l + [1] [1 1 1] [1] >= [1 1 1] [1] [0 0 0] @l + [0] [0 0 0] [0] = [c_11(sortAll^#(split(@l)))] Consider the set of all dependency pairs DPs: { 1: append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , 2: append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , 3: quicksort^#(@l) -> c_3(quicksort#1^#(@l)) , 4: quicksort#1^#(::(@z, @zs)) -> c_4(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , 5: quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_5(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , 6: splitqs^#(@pivot, @l) -> c_6(splitqs#1^#(@l, @pivot)) , 7: splitqs#1^#(::(@x, @xs), @pivot) -> c_7(splitqs^#(@pivot, @xs)) , 8: sortAll^#(@l) -> c_8(sortAll#1^#(@l)) , 9: sortAll#1^#(::(@x, @xs)) -> c_9(sortAll#2^#(@x, @xs)) , 10: sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_10(quicksort^#(@vals), sortAll^#(@xs)) , 11: splitAndSort^#(@l) -> c_11(sortAll^#(split(@l))) } Processor 'matrix interpretation of dimension 3' induces the complexity certificate YES(?,O(n^3)) on application of dependency pairs {4}. These cover all (indirect) predecessors of dependency pairs {4,5,11}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_3(quicksort#1^#(@l)) , splitqs^#(@pivot, @l) -> c_6(splitqs#1^#(@l, @pivot)) , splitqs#1^#(::(@x, @xs), @pivot) -> c_7(splitqs^#(@pivot, @xs)) } Weak DPs: { quicksort#1^#(::(@z, @zs)) -> c_4(quicksort#2^#(splitqs(@z, @zs), @z), splitqs^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_5(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , sortAll^#(@l) -> c_8(sortAll#1^#(@l)) , sortAll#1^#(::(@x, @xs)) -> c_9(sortAll#2^#(@x, @xs)) , sortAll#2^#(tuple#2(@vals, @key), @xs) -> c_10(quicksort^#(@vals), sortAll^#(@xs)) , splitAndSort^#(@l) -> c_11(sortAll^#(split(@l))) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(nil(), tuple#2(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) -> #false() , #eq(tuple#2(@x_1, @x_2), nil()) -> #false() , #eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , insert(@x, @l) -> insert#1(@x, @l, @x) , insert#1(tuple#2(@valX, @keyX), @l, @x) -> insert#2(@l, @keyX, @valX, @x) , insert#2(::(@l1, @ls), @keyX, @valX, @x) -> insert#3(@l1, @keyX, @ls, @valX, @x) , insert#2(nil(), @keyX, @valX, @x) -> ::(tuple#2(::(@valX, nil()), @keyX), nil()) , insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) -> insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x) , insert#4(#false(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(@vals1, @key1), insert(@x, @ls)) , insert#4(#true(), @key1, @ls, @valX, @vals1, @x) -> ::(tuple#2(::(@valX, @vals1), @key1), @ls) , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(splitqs(@z, @zs), @z) , quicksort#1(nil()) -> nil() , splitqs(@pivot, @l) -> splitqs#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split(@l) -> split#1(@l) , split#1(::(@x, @xs)) -> insert(@x, split(@xs)) , split#1(nil()) -> nil() , splitqs#1(::(@x, @xs), @pivot) -> splitqs#2(splitqs(@pivot, @xs), @pivot, @x) , splitqs#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitqs#2(tuple#2(@ls, @rs), @pivot, @x) -> splitqs#3(#greater(@x, @pivot), @ls, @rs, @x) , splitqs#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitqs#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Sequentially' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..